Nuprl Lemma : discrete-after-elapsed 11,40

es:event_system{i:l}, e:es-E(es), x:Id, T:Type.
es-dtype(es; loc(e); xT)
 (t:rationals. es-state-after-elapsed(eset)(x) = es-after(esxe T
latex


DefinitionsP  Q, es-dtype(esixT), quotient(Ax,y.B(x;y)), rationals, s = t, f(a), es-vartype(esix), x:AB(x), t  T, x:A  B(x), event_system{i:l}, t.1, es-E(es), atom{$n:n}, Id, Type, b, es_vartype(esix), es_state(esi), es-T(es), x:AB(x), P  Q, es_state_after(ese), es-state-after-elapsed(eset), prop{i:l}, es-state(esi), <ab>, sqequal(st), guard(T), sq_type(T), es-state-ap(sx), loc(e), es-after(esxe), #$n
Lemmasrationals wf, es-dtype wf, es-loc wf, Id wf, es-E wf, event system wf, es-isconst-property, int-rational, es state after wf, es state wf, es-state-after-elapsed wf, subtype rel wf, es-vartype wf

origin